;;; -*- Mode: LISP; Package: USER; Base: 10 -*-

(HERALD IO)

(DEFUN !CLAUSE-SET (CL-SET INDENT)
  (LET ((*INDENT* (OR INDENT *INDENT*)))
    (SETQ LAST-CLAUSE CL-SET)
    (PPRINDENT (COND ((NULL CL-SET) TRUE)
		     ((NULL (CDR CL-SET))
		      (PRETTYIFY-CLAUSE (CAR CL-SET)))
		     (T (CONS (QUOTE AND)
			      (LOOP FOR CL IN CL-SET
				    COLLECT (PRETTYIFY-CLAUSE CL)))))
	       (COND ((= 0 *INDENT*) 0)
		     (T (1+ *INDENT*)))
	       1 *FILE*)
    (SETQ LAST-PRINEVAL-CHAR NIL)
    NIL))

(DEFUN !CLAUSE (CL INDENT)
  (LET ((*INDENT* (OR INDENT *INDENT*)))
    (SETQ LAST-CLAUSE CL)
    (PPRINDENT (PRETTYIFY-CLAUSE CL)
	       (COND ((= 0 *INDENT*) 0)
		     (T (1+ *INDENT*)))
	       1 *FILE*)
    (SETQ LAST-PRINEVAL-CHAR NIL)
    NIL))

(DEFUN EQUALITY-HYP-NO (TERM CL)
  (LET (HYPS)
    (SETQ HYPS (LOOP FOR LIT IN CL
		     COUNT (MATCH LIT (NOT (EQUAL & &)))))
    (COND ((= HYPS 1)
	   NIL)
	  (T  (1+ (LOOP FOR LIT IN CL UNTIL (EQUAL LIT TERM)
			COUNT (MATCH LIT (NOT (EQUAL & &)))))))))

(DEFUN GET-SCHEMA-MEASURE-RELATION (CANDIDATE CL-SET)

;   Returns a list of three things.  A schematic formula, using p applied to
;   all the vars in CL-SET, showing the induction in CANDIDATE; a measure
;   term, indicating what decreases; and the well-founded relation.

  (LET (TERM MEASURE-ARGS FORMALS SCHEMA MEASURE RELATION)
    (SETQ TERM (ACCESS CANDIDATE INDUCTION-TERM CANDIDATE))
    (SETQ FORMALS (CADR (GET1 (FFN-SYMB TERM)
			      (QUOTE SDEFN))))
    (SETQ MEASURE (ACCESS JUSTIFICATION MEASURE-TERM
			  (ACCESS CANDIDATE JUSTIFICATION CANDIDATE)))

;   We must instantiate the measure term with the actuals.

    (SETQ MEASURE-ARGS (ALL-VARS MEASURE))
    (SETQ MEASURE (COND (MEASURE (SUB-PAIR-VAR-LST MEASURE-ARGS
						   (FILTER-ARGS MEASURE-ARGS
								FORMALS
								(FARGS TERM))
						   MEASURE))
			(T NIL)))
    (SETQ RELATION (ACCESS JUSTIFICATION RELATION
			   (ACCESS CANDIDATE JUSTIFICATION CANDIDATE)))
    (SETQ SCHEMA
	  (CONS
	    (QUOTE AND)
	    (LOOP FOR CL
		  IN
		  (IND-FORMULA
		    (ACCESS CANDIDATE TESTS-AND-ALISTS-LST CANDIDATE)
		    NIL
		    (LIST
		      (LIST
			(CONS
			  (QUOTE P)
			  (REVERSE
			    (ALL-VARS-LST
			      (REVERSE (APPLY (FUNCTION APPEND)
					      CL-SET))))))))
		  COLLECT (PRETTYIFY-CLAUSE CL))))
    (LIST SCHEMA MEASURE RELATION)))

(DEFUN IO (PROCESS PARENT PARENT-HIST DESCENDANTS HIST-ENTRY)
  (LET (TIME)
    (SETQ TIME (TIME-IN-60THS))
    (APPLY IO-FN NIL)
    (SETQ IOTHMTIME (PLUS IOTHMTIME (TIME-DIFFERENCE (TIME-IN-60THS)
						     TIME)))
    NIL))

(DEFUN IO1 NIL
  (PROG
    (SO-NEXT-CONSIDER ACCUMS CROSS DEFNS DIR ELIM-LEMMAS
		      GEN-LEMMAS HIGH-CNT INDENT KEEP LEMMAS LST
		      MASS MERGED-CAND-CNT N NAME NAMES OBVIOUS
		      RAW-CAND-CNT SKOS TERM1 TERM2 TERMS
		      WINNING-CAND WON-FLG VETO-CNT BROTHER-NO
		      MAX MEASURE RELATION SCHEMA FAVORED-CNT
		      HYP-NO FLG *NOPOINT)
    (SETQ *NOPOINT T)
    (SETQ SO-NEXT-CONSIDER
	  (PQUOTE
	    (PROGN
	      (COND ((EQ LAST-PROCESS (QUOTE POP))
		     /.))// // // /#
		     (COND ((NOT (EQ LAST-PROCESS (QUOTE STORE-SENT)))
			    (? (|so| |next| |consider|)
			       (|so| |let| |us| |turn| |our| |attention|
				     |to|)
			       (|so| |we| |now| |return| |to|))
			    /: // // (!CLAUSE-SET CL-SET INDENT)
			    (? (/, // // |named|)
			       (/, // // |which| |we| |named|)
			       (/, // // |which| |is| |formula|))
			    (!PPR (CAR HIST-ENTRY) NIL)
			    |above| /.)
			   ((AND (= (LENGTH CL-SET) 1)
				 (EQ LAST-CLAUSE (CAR CL-SET))))
			   (T |so| |now| |let| |us| (? (|consider|)
						       (|return| |to|))
			      /: // // (!CLAUSE-SET CL-SET NIL)
			      (? (/, // // |named|)
				 (/, // // |which| |we| |named|)
				 (/. // // |we| |named| |this|)
				 (/. // // |we| |gave| |this| |the| |name|))
			      (!PPR (CAR HIST-ENTRY) NIL)
			      (? (|above|)
				 NIL)
			      /.)))))
    (COND ((EQ PROCESS (QUOTE SETUP))
	   (COND ((NOT (OPENP PROVE-FILE))
		  (SETQ PROVE-FILE NIL)))
	   (SETQ CLAUSE-ALIST NIL)
	   (SETQ LAST-PROCESS (QUOTE SETUP))
	   (SETQ LAST-PRINEVAL-CHAR (QUOTE /.))
	   (NOTICE-CLAUSE PARENT 0 (LIST NIL)))
	  ((EQ PROCESS (QUOTE SETTLED-DOWN-CLAUSE))
	   (RETURN NIL))
	  ((EQ PROCESS (QUOTE INDUCT))
	   (COND ((AND (NOT LEFTMARGINCHAR)
		       (EQ PARENT LAST-CLAUSE))
		  (SETQ TEMP-TEMP (UN-NOTICE-CLAUSE LAST-CLAUSE))
		  (SETQ CLAUSE-ALIST NIL)
		  (COND ((AND (FIXP (CADR TEMP-TEMP))
			      (LESSP (CADR TEMP-TEMP)
				     16))
			 (NOTICE-CLAUSE LAST-CLAUSE (CADR TEMP-TEMP)
					(LIST NIL)))
			(T (NOTICE-CLAUSE (CAR TEMP-TEMP)
					  0
					  (LIST NIL)))))
		 (T (SETQ CLAUSE-ALIST NIL)
		    (NOTICE-CLAUSE PARENT 0 (LIST NIL))))))
    (SETQ TEMP-TEMP
	  (COND ((AND PARENT
		      (NOT (MEMQ PROCESS
				 (QUOTE (POP SUBSUMED-ABOVE
					     SUBSUMED-BY-PARENT
					     SUBSUMED-BELOW)))))
		 (UN-NOTICE-CLAUSE PARENT))
		(T (QUOTE (NIL 0 (NIL))))))

;   The BROTHER-NO of a clause is the case number for it.  It is a list of
;   numbers, to be printed in reverse order, separated by dots.  If the CAR of
;   the BROTHER-NO is NIL it means do not print it.

    (SETQ BROTHER-NO (OR (CADDR TEMP-TEMP)
			 (LIST NIL)))
    (SETQ INDENT (CADR TEMP-TEMP))
    (SETQ MAX (LENGTH DESCENDANTS))
    (LOOP FOR CL IN DESCENDANTS AS I FROM MAX BY -1
	  DO (NOTICE-CLAUSE CL (COND ((= MAX 1)
				      INDENT)
				     (T (+ TREE-INDENT INDENT)))
			    (COND ((= MAX 1)
				   (COND ((CAR BROTHER-NO)
					  (CONS NIL BROTHER-NO))
					 (T BROTHER-NO)))
				  ((CAR BROTHER-NO)
				   (CONS I BROTHER-NO))
				  (T (CONS I (CDR BROTHER-NO))))))
    (COND ((MEMQ PROCESS EXECUTE-PROCESSES)
	   (COND ((EQ LAST-PROCESS (QUOTE SETUP))
		  (SETQ LAST-CLAUSE PARENT))
		 (T (ITERPRIN TREE-LINES PROVE-FILE)
		    (ISPACES (- INDENT TREE-INDENT)
			     PROVE-FILE)
		    (COND ((AND (NOT (EQUAL INDENT 0))
				(CAR BROTHER-NO))
			   (IPRINC (QUOTE |Case |) PROVE-FILE)
			   (LOOP FOR I IN (REVERSE BROTHER-NO)
				 DO (IPRINC I PROVE-FILE)
				 (IPRINC (QUOTE /.)
					 PROVE-FILE))))
		    (PRINEVAL (PQUOTE (!CLAUSE PARENT NIL))
			      (BINDINGS (QUOTE PARENT)
					PARENT)
			      (+ 5 INDENT)
			      PROVE-FILE)))))
    (SELECTQ
      PROCESS
      (SIMPLIFY-CLAUSE
       (SETQ FLG NIL)
       (SETQ LEMMAS NIL)
       (SETQ DEFNS NIL)
       (LOOP FOR X IN HIST-ENTRY
	     DO (COND ((PAIRP X)

;   A PAIRP entry here means that PROCESS-EQUATIONAL-POLYS added an equality to
;   this clause.  The form of X in this case is ((FIND-EQUATIONAL-POLY lhs .
;   rhs)), where lhs and rhs are the sides of the equation added.  In this
;   case, ZERO is also a member of HIST-ENTRY and at the moment we will just
;   ignore this opportunity to make the IO fancier.

		       NIL)
		      ((EQ X (QUOTE ZERO))
		       (SETQ FLG T))
		      ((GET1 X (QUOTE TYPE-PRESCRIPTION-LST))
		       (SETQ DEFNS (CONS X DEFNS)))
		      (T (SETQ LEMMAS (CONS X LEMMAS)))))
       (COND ((AND (EQ LAST-PROCESS (QUOTE SETUP))
		   (= (LENGTH DESCENDANTS) 1)
		   (NOT LEMMAS)
		   (LOOP FOR X IN DEFNS
			 ALWAYS (MEMQ X (QUOTE (AND OR NOT IMPLIES))))
		   (NOT FLG))

;   pretend nothing happened in this case.

	      (RPLACA (CDR (ASSQ (CAR DESCENDANTS)
				 CLAUSE-ALIST))
		      0)
	      (RETURN NIL))
	     (T
	      (PRINEVAL
		(PQUOTE
		  (PROGN
		    (COND ((EQ LAST-PROCESS (QUOTE SETUP))
			   |this|
			   (? (|formula|)
			      (|conjecture|)
			      NIL)
			   |simplifies|)
			  (T (? (/, // // |which| (? (|we| (@ FURTHER?)
							   |simplify|)
						     ((@ FURTHER?)
						      |simplifies|)))
				(/. // //(COND ((EQ HIST-ENTRY NIL)
						(? NIL (|of| |course| /,)))
					       (PARENT-HIST
						(? (|but|)
						   NIL
						   (|however|))))
				    |this|
				    (? (|simplifies| (@ FURTHER?))
				       ((@ FURTHER?)
					|simplifies|))))))
		    (COND (FLG /, |using| |linear| |arithmetic|
			       (COND ((AND (NOT LEMMAS)
					   (NOT DEFNS))
				      /,))))
		    (COND (LEMMAS (COND ((AND FLG (NOT DEFNS))
					 |and|)
					(T /,))
				  (? ((? (|appealing| |to|)
					 (|applying|)
					 (|rewriting| |with|))
				      |the|
				      (PLURAL? LEMMAS |lemmas| |lemma|))
				     (|applying|)
				     (|rewriting| |with|))
				  (!LIST LEMMAS)
				  /,))
		    (COND (DEFNS (COND ((OR FLG LEMMAS)
					|and|)
				       (T /,))
				 (? (|opening| |up|)
				    (|expanding|)
				    (|unfolding|))
			    (? (|the| (PLURAL? DEFNS |functions|
					       |function|))
			       (|the| (PLURAL? DEFNS |definitions|
					       |definition|)
				      |of|)
			       NIL)
			    (!LIST DEFNS)
			    /,))
		    (COND ((AND (NOT FLG)
				(EQ LEMMAS NIL)
				(EQ DEFNS NIL))
			   /,
			   (? (|trivially|)
			      (|clearly|)
			      (|obviously|))
			   /,))
		    |to|))
		(BINDINGS (QUOTE DEFNS)
			  DEFNS
			  (QUOTE LEMMAS)
			  LEMMAS
			  (QUOTE PARENT-HIST)
			  PARENT-HIST
			  (QUOTE HIST-ENTRY)
			  HIST-ENTRY
			  (QUOTE FURTHER?)
			  (COND ((AND (NOT DESCENDANTS)
				      (> (LENGTH PARENT-HIST)
						5))
				 (PQUOTE |finally|))
				((EQ (CAAR PARENT-HIST)
				     (QUOTE SIMPLIFY-CLAUSE))
				 (PQUOTE |again|))
				((ASSQ (QUOTE SIMPLIFY-CLAUSE)
				       PARENT-HIST)
				 (PQUOTE |further|))
				(T NIL))
			  (QUOTE LAST-PROCESS)
			  LAST-PROCESS
			  (QUOTE FLG)
			  FLG)
		INDENT PROVE-FILE))))
      (FERTILIZE-CLAUSE (MATCH HIST-ENTRY
			       (LIST MASS CROSS DIR TERM1 TERM2
				     KEEP))
			(SETQ HYP-NO
			      (EQUALITY-HYP-NO
				(LIST (QUOTE NOT)
				      (LIST (QUOTE EQUAL)
					    TERM1 TERM2))
				PARENT))
			(OR (EQ DIR (QUOTE LEFT-FOR-RIGHT))
			    (SWAP TERM1 TERM2))
			(PRINEVAL
			  (PQUOTE (PROGN /. // // |we| (? NIL NIL
							  (|now|))
					 |use| |the|
					 (COND (HYP-NO (@ N))
					       (T |above|))
					 |equality| |hypothesis|
					 (COND ((OR MASS (NOT CROSS))
						|by| |substituting|)
					       (T |by|
						  |cross-fertilizing|))
					 (!PPR TERM1 NIL)
					 |for|
					 (!PPR TERM2 NIL)
					 (COND (KEEP |and| |keeping| |the|
						     |equality|
						     |hypothesis|)
					       (T |and| |throwing| |away|
						  |the| |equality|))
					 /.))
			  (BINDINGS (QUOTE KEEP)
				    KEEP
				    (QUOTE TERM2)
				    TERM2
				    (QUOTE TERM1)
				    TERM1
				    (QUOTE CROSS)
				    CROSS
				    (QUOTE MASS)
				    MASS
				    (QUOTE N)
				    (TH-IFY HYP-NO)
				    (QUOTE HYP-NO)
				    HYP-NO)
			  INDENT PROVE-FILE))
      (ELIMINATE-DESTRUCTORS-CLAUSE
       (SETQ ELIM-LEMMAS NIL)
       (SETQ GEN-LEMMAS NIL)
       (LOOP FOR X IN HIST-ENTRY
	     DO
	     (SETQ ELIM-LEMMAS (ADD-TO-SET (CAR X)
					   ELIM-LEMMAS))
	     (SETQ LST
		   (CONS (LIST (QUOTE PROGN)
			       (LIST (QUOTE !PPR)
				     (KWOTE (CAR (CDDDDR X)))
				     NIL)
			       (PQUOTE |by|)
			       (LIST (QUOTE !PPR)
				     (KWOTE (CADR (CDDDDR X)))
				     NIL)
			       (PQUOTE (PROGN |to| |eliminate|))
			       (LIST (QUOTE !LIST)
				     (KWOTE (LOOP FOR D IN (CADR X)
						  COLLECT
						  (LIST (QUOTE !PPR)
							(KWOTE D)
							NIL)))))
			 LST))
	     (COND ((CADDR X)
		    (SETQ
		      GEN-LEMMAS
		      (UNION-EQUAL
			(LOOP FOR TERM IN (CADDR X)
			      WITH LOOP-ANS
			      DO
			      (SETQ
				LOOP-ANS
				(ADD-TO-SET
				  (LIST (QUOTE PROGN)
					(PQUOTE (PROGN |the| |type|
						       |restriction|
						       |lemma| |noted|
						       |when|))
					(FN-SYMB (ARGN TERM 1))
					(PQUOTE (PROGN |was| |introduced|)))
				  LOOP-ANS))
			      FINALLY (RETURN LOOP-ANS))
			GEN-LEMMAS))))
	     (SETQ GEN-LEMMAS (UNION-EQUAL (CADDDR X)
					   GEN-LEMMAS)))
       (PRINEVAL
	 (PQUOTE
	   (PROGN /. // //(? (|applying|)
			     (|appealing| |to|))
		  |the|
		  (PLURAL? ELIM-LEMMAS |lemmas| |lemma|)
		  (!LIST ELIM-LEMMAS)
		  /,
		  (? (|we| |now|)
		     NIL)
		  |replace|
		  (!LIST LST)
		  /.
		  (COND (GEN-LEMMAS
			 |we|
			 (? (|use|)
			    (|rely| |upon|)
			    (|employ|))
			 (!LIST GEN-LEMMAS)
			 |to|
			 (? (|constrain|)
			    (|restrict|))
			 |the| |new|
			 (COND ((OR (CDR ELIM-LEMMAS)
				    (CDR (CAR (CDR (CAR HIST-ENTRY)))))
				|variables|)
			       (T |variable|))
			 /.))))
	 (BINDINGS (QUOTE HIST-ENTRY)
		   HIST-ENTRY
		   (QUOTE ELIM-LEMMAS)
		   ELIM-LEMMAS
		   (QUOTE GEN-LEMMAS)
		   GEN-LEMMAS
		   (QUOTE LST)
		   LST)
	 INDENT PROVE-FILE))
      (GENERALIZE-CLAUSE
       (MATCH HIST-ENTRY (LIST SKOS TERMS OBVIOUS LEMMAS))
       (SETQ LST (LOOP FOR TERM IN TERMS AS VAR IN SKOS
		       COLLECT (LIST (QUOTE PROGN)
				     (LIST (QUOTE !PPR)
					   (KWOTE TERM)
					   NIL)
				     (PQUOTE |by|)
				     (LIST (QUOTE !PPR)
					   (KWOTE VAR)
					   NIL))))
       (COND (OBVIOUS
	      (SETQ
		LEMMAS
		(UNION-EQUAL
		  (LOOP FOR TERM IN OBVIOUS
			WITH LOOP-ANS
			DO
			(SETQ LOOP-ANS
			      (ADD-TO-SET
				(LIST (QUOTE PROGN)
				      (PQUOTE (PROGN |the| |type|
						     |restriction|
						     |lemma| |noted|
						     |when|))
				      (FN-SYMB (ARGN TERM 1))
				      (PQUOTE (PROGN |was|
						     |introduced|)))
				LOOP-ANS))
			FINALLY (RETURN LOOP-ANS))
		  LEMMAS))))
       (PRINEVAL (PQUOTE (PROGN (? (/, // // |which| |we| |generalize| |by|)
				   (/. // // |we| |will| |try| |to| |prove|
				       |the| |above| (? (|formula|)
							(|conjecture|))
				       |by| |generalizing| |it| /,))
				|replacing|
				(!LIST LST)
				/.
				(COND (LEMMAS |we| |restrict| |the| |new|
					      (PLURAL? SKOS
						       |variables|
						       |variable|)
					      |by|
					      (? (|appealing| |to|)
						 (|recalling|))
					      (!LIST LEMMAS)
					      /.))))
		 (BINDINGS (QUOTE LEMMAS)
			   LEMMAS
			   (QUOTE SKOS)
			   SKOS
			   (QUOTE LST)
			   LST)
		 INDENT PROVE-FILE))
      (ELIMINATE-IRRELEVANCE-CLAUSE
       (PRINEVAL (PQUOTE (? (/, // // |which| |has| (PLURAL? N
							     (@ N)
							     |an|)
				|irrelevant|
				(PLURAL? N |terms| |term|)
				|in| |it| /. |by| |eliminating|
				(PLURAL? N (PROGN |these| |terms|)
					 (PROGN |the| |term|))
				|we| |get|)
			    (/. // // |eliminate|
				(PLURAL? N NIL |the|)
				|irrelevant|
				(PLURAL? N |terms| |term|)
				/.)))
		 (BINDINGS (QUOTE N)
			   (- (LENGTH PARENT)
			      (LENGTH (CAR DESCENDANTS))))
		 INDENT PROVE-FILE))
      (STORE-SENT (NOTICE-CLAUSE PARENT INDENT BROTHER-NO)
		  (COND ((AND PARENT (EQ LAST-PROCESS (QUOTE SETUP))
			      (CADR HIST-ENTRY))
			 (SETQ LAST-CLAUSE (CADR HIST-ENTRY))
			 (NOTICE-CLAUSE LAST-CLAUSE 0 (LIST NIL))))
		  (PRINEVAL (PQUOTE
			      (COND ((EQ PARENT NIL)
				     (? (/, // // |which| |means|
					    |the|
					    |proof| |attempt| |has|)
					(/. // // |why| |say|
					    |more| ?)
					(/. // // |need|
					    |we| |go| |on|
					    ?)))
				    ((EQ LAST-PROCESS
					 (QUOTE SETUP))
				     // /#
				     (? (|give| |the| |conjecture|
						|the| |name|)
					(|name| |the| |conjecture|)
					(|call| |the| |conjecture|))
				     (!PPR (CAR HIST-ENTRY) NIL)
				     /.)
				    ((EQ (CAR (CDR HIST-ENTRY))
					 (QUOTE QUIT))
				     /, // // |which| |we| |would|
				     |normally| |try| |to|
				     |prove| |by|
				     |induction| /. |But| |since|
				     |the|
				     DO-NOT-USE-INDUCTION-FLG |has|
				     |been| |set| |by| |the| |user| /,
				     |the| |proof| |attempt| |has|)
				    ((CAR (CDR HIST-ENTRY))
				     /, // // |which| |we| |would|
				     (? (|normally|)
					(|usually|))
				     |push| |and| |work|
				     |on| |later| |by|
				     |induction| /. |But| |if| |we|
				     |must| |use| |induction| |to|
				     |prove| |the| |input|
				     |conjecture| /, |we|
				     |prefer| |to|
				     |induct| |on| |the| |original|
				     |formulation| |of| |the|
				     |problem| /. |Thus| |we| |will|
				     |disregard| |all| |that| |we|
				     |have| |previously| |done| /,
				     |give| |the| |name|
				     (!PPR (CAR HIST-ENTRY) NIL)
				     |to| |the| |original| |input| /,
				     |and| |work| |on| |it| /.)
				    (T (? (/, // // |which| |we|
					      |will| (@ FINALLY?) |name|
					      (!PPR (CAR HIST-ENTRY) NIL)
					      /.)
					  (/. // //(@ FINALLY?)
					      (? (|give| |the|
							 |above|
							 |formula|
							 |the|
							 |name|)
						 (|name| |the|
							 |above|
							 |subgoal|)
						 (|call| |the|
							 |above|
							 |conjecture|))
					      (!PPR (CAR HIST-ENTRY) NIL)
					      /.)))))
			    (BINDINGS
			      (QUOTE HIST-ENTRY)
			      HIST-ENTRY
			      (QUOTE LAST-PROCESS)
			      LAST-PROCESS
			      (QUOTE PARENT)
			      PARENT
			      (QUOTE FINALLY?)
			      (COND ((> (LENGTH PARENT-HIST)
					       5)
				     (PQUOTE |finally|))
				    (T NIL)))
			    INDENT PROVE-FILE))
      (POP (PRINEVAL (PQUOTE (PROGN (COND ((EQ LAST-PROCESS
					       (QUOTE POP))
					   /, |which|
					   (? (/, |in| |turn| /,)
					      (/, |consequently| /,)
					      NIL)
					   (? (|also|)
					      NIL))
					  (T // // // /# |that|))
				    |finishes| |the| |proof| |of|
				    (!PPR (CAR HIST-ENTRY) NIL)))
		     (BINDINGS (QUOTE HIST-ENTRY)
			       HIST-ENTRY
			       (QUOTE LAST-PROCESS)
			       LAST-PROCESS)
		     0 PROVE-FILE))
      (SUBSUMED-ABOVE
       (PRINEVAL
	 (PQUOTE (PROGN (@ SO-NEXT-CONSIDER)
			(? (|ha| !)
			   (|how| |nice| !)
			   NIL NIL NIL)
			|this|
			(? (|conjecture|)
			   (|formula|)
			   (|goal|)
			   NIL)
			|is| |subsumed| |by| |the|
			(? ((? (|lemma|)
			       (|theorem|)
			       (|goal|))
			    |we| |named| (!PPR (CAR (CDR HIST-ENTRY))
					       NIL)
			    |and| |proved| |above|)
			   (|previously| |proved|
					 (!PPR (CAR (CDR HIST-ENTRY))
					       NIL))
			   ((!PPR (CAR (CDR HIST-ENTRY)) NIL)
			    /, |which| |was| |proved| |above|))
			!))
	 (BINDINGS (QUOTE HIST-ENTRY)
		   HIST-ENTRY
		   (QUOTE SO-NEXT-CONSIDER)
		   SO-NEXT-CONSIDER
		   (QUOTE LAST-PROCESS)
		   LAST-PROCESS
		   (QUOTE CL-SET)
		   PARENT
		   (QUOTE LAST-CLAUSE)
		   LAST-CLAUSE
		   (QUOTE INDENT)
		   5)
	 0 PROVE-FILE))
      (SUBSUMED-BY-PARENT
       (PRINEVAL (PQUOTE (PROGN (@ SO-NEXT-CONSIDER)
				(? (|oh| |no| !)
				   (|oops| !)
				   NIL)
				|this| |formula| |is| |subsumed| |by| |its|
				|parent| /,
				(!PPR (CAR (CDR HIST-ENTRY)) NIL)
				!(? (|that| |means| |we| |would|
					    |loop| |if| |we|
					    |tried| |to| |prove| |it| |by|
					    |induction| /.)
				    NIL NIL)))
		 (BINDINGS (QUOTE HIST-ENTRY)
			   HIST-ENTRY
			   (QUOTE SO-NEXT-CONSIDER)
			   SO-NEXT-CONSIDER
			   (QUOTE LAST-PROCESS)
			   LAST-PROCESS
			   (QUOTE CL-SET)
			   PARENT
			   (QUOTE LAST-CLAUSE)
			   LAST-CLAUSE
			   (QUOTE INDENT)
			   5)
		 0 PROVE-FILE))
      (SUBSUMED-BELOW (PRINEVAL
			(PQUOTE (PROGN (@ SO-NEXT-CONSIDER)
				       (? (|ah| |ha| !)
					  (|what| |luck| !)
					  (|you| |probably| |did| |not|
						 |notice| /, |but|)
					  (|but|)
					  NIL)
				       |this| |conjecture| |is|
				       |subsumed| |by|
				       (? (|another| |subgoal|
						     |awaiting| |our|
						     |attention| /,
						     |namely|)
					  (|the| |subgoal| |we| |named|)
					  (|formula|))
				       (!PPR (CAR (CDR HIST-ENTRY)) NIL)
				       |above| /.))
			(BINDINGS (QUOTE HIST-ENTRY)
				  HIST-ENTRY
				  (QUOTE SO-NEXT-CONSIDER)
				  SO-NEXT-CONSIDER
				  (QUOTE LAST-PROCESS)
				  LAST-PROCESS
				  (QUOTE CL-SET)
				  PARENT
				  (QUOTE LAST-CLAUSE)
				  LAST-CLAUSE
				  (QUOTE INDENT)
				  5)
			0 PROVE-FILE))
      (INDUCT
       (MATCH HIST-ENTRY
	      (LIST NAME WINNING-CAND RAW-CAND-CNT
		    MERGED-CAND-CNT VETO-CNT HIGH-CNT
		    FAVORED-CNT))
       (COND
	 (WINNING-CAND
	  (SETQ FLG NIL)
	  (SETQ LEMMAS NIL)
	  (SETQ DEFNS NIL)
	  (LOOP FOR X
		IN (ACCESS JUSTIFICATION LEMMAS
			   (ACCESS CANDIDATE
				   JUSTIFICATION WINNING-CAND))
		DO (COND ((EQ X (QUOTE ZERO))
			  (SETQ FLG T))
			 ((GET1 X (QUOTE TYPE-PRESCRIPTION-LST))
			  (SETQ DEFNS (CONS X DEFNS)))
			 (T (SETQ LEMMAS (CONS X LEMMAS)))))
	  (MATCH (GET-SCHEMA-MEASURE-RELATION WINNING-CAND
					      PARENT)
		 (LIST SCHEMA MEASURE RELATION))
	  (SETQ ACCUMS
		(SET-DIFF (ACCESS CANDIDATE CHANGED-VARS WINNING-CAND)
			  (ALL-VARS MEASURE)))
	  (PRINEVAL
	    (PQUOTE
	      (PROGN
		(@ SO-NEXT-CONSIDER)
		(? (|we| |will| |try| |to| |prove| |it|
			 |by| |induction|
			 /.)
		   (|perhaps| |we| |can| |prove| |it| |by|
			      |induction|
			      /.)
		   (|let| |us| |appeal| |to| |the| |induction|
			  |principle| /.)
		   (|we| |will| |appeal| |to| |induction| /.))
		(COND
		  ((NOT (= RAW-CAND-CNT 1))
		   (? (|there| |are| (@ RAW-CAND-CNT)
			       |plausible| |inductions|)
		      ((@ RAW-CAND-CNT)
		       |inductions| |are|
		       |suggested| |by| |terms|
		       |in| |the| |conjecture|)
		      (|the| |recursive| |terms| |in| |the|
			     |conjecture| |suggest|
			     (@ RAW-CAND-CNT)
			     |inductions|))
		   (COND ((= RAW-CAND-CNT MERGED-CAND-CNT))
			 ((= MERGED-CAND-CNT 1)
			  /. |However| /, |they|
			  |merge| |into| |one|
			  |likely| |candidate| |induction| /.)
			 (T /. |They| |merge| |into|
			    (@ MERGED-CAND-CNT)
			    |likely| |candidate| |inductions|))
		   (COND
		     ((NOT (= MERGED-CAND-CNT 1))
		      (COND ((= VETO-CNT 0)
			     /,
			     (COND ((= MERGED-CAND-CNT 2)
				    |both|)
				   (T |all|))
			     |of| |which| |are|
			     |flawed| /.)
			    ((= VETO-CNT MERGED-CAND-CNT)
			     /,
			     (COND ((= VETO-CNT 2)
				    |both|)
				   (T |all|))
			     |of| |which| |are|
			     |unflawed| /.)
			    ((= VETO-CNT 1)
			     /. |however| /, |only|
			     |one| |is|
			     |unflawed| /.)
			    (T /, (@ VETO-CNT)
			       |of| |which|
			       |are| |unflawed| /.))
		      (COND
			((NOT (= VETO-CNT 1))
			 (COND ((= FAVORED-CNT 1)
				|so| |we|
				|will| |choose|
				|the| |one|
				|suggested| |by|
				|the| |largest|
				|number| |of|
				|nonprimitive|
				|recursive| |functions| /.)
			       (T (COND ((NOT (= FAVORED-CNT
						     VETO-CNT))
					 |we| |limit| |our|
					 |consideration| |to| |the|
					 (@ FAVORED-CNT)
					 |suggested| |by| |the|
					 |largest| |number| |of|
					 |nonprimitive|
					 |recursive| |functions|
					 |in| |the| |conjecture| /.))
				  (COND ((= HIGH-CNT 1)
					 |however| /, |one| |of|
					 |these| |is| |more| |likely|
					 |than| |the|
					 (COND ((= FAVORED-CNT 2)
						|other|)
					       (T |others|))
					 /.)
					(T |since|
					   (COND ((= HIGH-CNT
							 FAVORED-CNT)
						  (COND ((= HIGH-CNT
								2)
							 |both|)
							(T |all|)))
						 (T (@ HIGH-CNT)))
					   |of| |these| |are| |equally|
					   |likely| /, |we| |will|
					   |choose| |arbitrarily|
					   /.)))))))))
		  (T |there| |is| |only| |one| (? (|plausible|)
						  (|suggested|))
		     |induction| /.))
		|we| |will| |induct| |according| |to| |the| |following|
		|scheme| (!PPR SCHEMA (PQUOTE /.))
		(COND (MEASURE (@ JUSTIFICATION-SENTENCE)
			       (PLURAL? TESTS-AND-ALISTS-LST
					|each| |the|)
			       |induction| |step| |of| |the| |scheme| /.
			       (COND (ACCUMS |note| /, |however| /, |the|
					     |inductive|
					     (COND (INSTANCES?
						    |instances|)
						   (T |instance|))
					     |chosen| |for|
					     (!PPR-LIST ACCUMS)
					     /.))
			       |the| |above| |induction| |scheme|
			       (? (|produces|)
				  (|generates|)
				  (|leads| |to|)))
		      (T |this| |scheme| |is| |justified| |by| |the|
			 |assumption| |that| (!PPR (FN-SYMB TERM) NIL)
			 |is| |total| /.))))
	    (BINDINGS (QUOTE ACCUMS)
		      ACCUMS
		      (QUOTE JUSTIFICATION-SENTENCE)
		      (JUSTIFICATION-SENTENCE)
		      (QUOTE RELATION)
		      RELATION
		      (QUOTE MEASURE)
		      MEASURE
		      (QUOTE LEMMAS)
		      LEMMAS
		      (QUOTE DEFNS)
		      DEFNS
		      (QUOTE FLG)
		      FLG
		      (QUOTE NUMBER)
		      (LENGTH (ACCESS JUSTIFICATION LEMMAS
				      (ACCESS CANDIDATE JUSTIFICATION
					      WINNING-CAND)))
		      (QUOTE SCHEMA)
		      SCHEMA
		      (QUOTE FAVORED-CNT)
		      FAVORED-CNT
		      (QUOTE HIGH-CNT)
		      HIGH-CNT
		      (QUOTE MERGED-CAND-CNT)
		      MERGED-CAND-CNT
		      (QUOTE VETO-CNT)
		      VETO-CNT
		      (QUOTE RAW-CAND-CNT)
		      RAW-CAND-CNT
		      (QUOTE SO-NEXT-CONSIDER)
		      SO-NEXT-CONSIDER
		      (QUOTE TESTS-AND-ALISTS-LST)
		      (ACCESS CANDIDATE TESTS-AND-ALISTS-LST
			      WINNING-CAND)
		      (QUOTE INSTANCES?)
		      (OR (CDR ACCUMS)
			  (NOT (= 1
				      (LOOP FOR TA
					    IN (ACCESS CANDIDATE
						       TESTS-AND-ALISTS-LST
						       WINNING-CAND)
					    SUM (LENGTH (ACCESS
							 TESTS-AND-ALISTS
							 ALISTS TA))))))
		      (QUOTE TERM)
		      (ACCESS CANDIDATE INDUCTION-TERM WINNING-CAND)
		      (QUOTE LAST-PROCESS)
		      LAST-PROCESS
		      (QUOTE CL-SET)
		      PARENT
		      (QUOTE LAST-CLAUSE)
		      LAST-CLAUSE
		      (QUOTE HIST-ENTRY)
		      HIST-ENTRY
		      (QUOTE INDENT)
		      (+ 5 INDENT))
	    INDENT PROVE-FILE))
	 (T (PRINEVAL (PQUOTE (PROGN (@ SO-NEXT-CONSIDER)
				     |since| |there| |is| |nothing| |to|
				     |induct| |upon| /, |the| |proof| |has|))
		      (BINDINGS (QUOTE SO-NEXT-CONSIDER)
				SO-NEXT-CONSIDER
				(QUOTE LAST-PROCESS)
				LAST-PROCESS
				(QUOTE CL-SET)
				PARENT
				(QUOTE LAST-CLAUSE)
				LAST-CLAUSE
				(QUOTE HIST-ENTRY)
				HIST-ENTRY
				(QUOTE INDENT)
				5)
		      0 PROVE-FILE))))
      (SETUP
       (COND ((AND (= (LENGTH DESCENDANTS) 1)
		   (LOOP FOR X IN HIST-ENTRY
			 ALWAYS (MEMQ X (QUOTE (AND OR NOT IMPLIES)))))
	      NIL)
	     (T (PRINEVAL
		  (PQUOTE (PROGN |this| (? (|formula|)
					   (|conjecture|))
				 |can| |be|
				 (COND (HIST-ENTRY |simplified| /, |using|
						   |the|
						   (PLURAL? HIST-ENTRY
							    |abbreviations|
							    |abbreviation|)
						   (!LIST HIST-ENTRY)
						   /,)
				       (T |propositionally| |simplified|))
				 |to|))
		  (BINDINGS (QUOTE HIST-ENTRY)
			    HIST-ENTRY)
		  INDENT PROVE-FILE))))
      (FINISHED (MATCH HIST-ENTRY (LIST WON-FLG))
		(PRINEVAL (PQUOTE
			    (PROGN (COND ((EQ LAST-PROCESS
					      (QUOTE POP))
					  /.
					  (COND (WON-FLG |Q.E.D.|)
						(T // // (@ FAILURE-MSG))))
					 (T // //
					    (COND ((EQ WON-FLG
						       (QUOTE DEFN-OK)))
						  (WON-FLG |Q.E.D.|)
						  (T (@ FAILURE-MSG))))) //
				   //))
			  (BINDINGS (QUOTE FAILURE-MSG)
				    FAILURE-MSG
				    (QUOTE WON-FLG)
				    WON-FLG
				    (QUOTE LAST-PROCESS)
				    LAST-PROCESS)
			  0 PROVE-FILE))
      (OTHERWISE
       (ERROR1 (PQUOTE (PROGN IO1 |has| |been| |given| |an| |unrecognized|
			      |process| |named| (!PPR PROCESS NIL)
			      /.))
	       (BINDINGS (QUOTE PROCESS)
			 PROCESS)
	       (QUOTE HARD))))
    (COND ((NOT (OR (MEMQ PROCESS UN-PRODUCTIVE-PROCESSES)
		    (AND (EQ PROCESS (QUOTE INDUCT))
			 (NOT (CADR HIST-ENTRY)))
		    (AND (EQ PROCESS (QUOTE SETUP))
			 (= (LENGTH DESCENDANTS) 1)
			 (LOOP FOR X IN HIST-ENTRY
			       ALWAYS (MEMQ X
					    (QUOTE (AND OR NOT IMPLIES)))))))
	   (SETQ N (LENGTH DESCENDANTS))
	   (COND ((EQ LAST-PRINEVAL-CHAR (QUOTE /.))
		  (PRINEVAL (PQUOTE (? (|we| |thus| |obtain|)
				       (|the| |result| |is|)
				       (|this| |produces|)
				       (|this| |generates|)
				       (|we| |would| |thus| |like| |to|
					     |prove|)
				       (|we| |must| |thus| |prove|)))
			    (BINDINGS)
			    INDENT PROVE-FILE)))
	   (COND ((NEQ LAST-PRINEVAL-CHAR (QUOTE /:))
		  (PRINEVAL (PQUOTE (PROGN (COND ((EQUAL N 0)
						  NIL)
						 ((EQUAL N 1)
						  (? (|the| (? (|new|)
							       NIL)
							    (? (|goal|)
							       (|conjecture|)
							       (|formula|)))
						     NIL NIL))
						 (T
						  (? ((@ N)
						      |new|
						      (? (|goals|)
							 (|conjectures|)
							 (|formulas|)))
						     (|the|
						       |following|
						       (@ N)
						       |new|
						       (? (|goals|)
							  (|conjectures|)
							  (|formulas|))))))/:))
			    (BINDINGS (QUOTE N)
				      N)
			    INDENT PROVE-FILE)))))
    (COND ((AND (NOT (MEMQ PROCESS UN-PRODUCTIVE-PROCESSES))
		(NOT DESCENDANTS))
	   (ITERPRIN TREE-LINES PROVE-FILE)
	   (PRINEVAL (PQUOTE (PROGN T /.))
		     (BINDINGS)
		     (+ 6 INDENT)
		     PROVE-FILE)))
    (SETQ LAST-PROCESS
	  (COND ((AND (EQ PROCESS (QUOTE SETUP))
		      (OR (NOT (= (LENGTH DESCENDANTS) 1))
			  (NOT (LOOP FOR X IN HIST-ENTRY
				     ALWAYS (MEMQ X
						  (QUOTE (AND OR NOT
							      IMPLIES)))))))
		 (QUOTE SETUP-AND-CLAUSIFY-INPUT))
		(T PROCESS)))
    (RETURN NIL)))

(DEFUN JUSTIFICATION-SENTENCE NIL

;   This fn returns a sentence to be fed to PRINEVAL.  The BINDINGS must
;   include FLG, LEMMAS, DEFNS, NUMBER, MEASURE, and RELATION.  FLG is T or NIL
;   indicating that linear arithmetic was used.  LEMMAS and DEFNS are the list
;   of lemmas and definitions used.  NUMBER is the length of LEMMAS plus that
;   of DEFNS plus 1 or 0 according to FLG.  MEASURE is a term and RELATION is a
;   fn name.

  (PQUOTE (PROGN (COND (FLG |linear| |arithmetic| (COND ((AND LEMMAS DEFNS)
							 /,)
							((OR LEMMAS DEFNS)
							 |and|))))
		 (COND (LEMMAS |the| (PLURAL? LEMMAS |lemmas| |lemma|)
			       (!LIST LEMMAS)
			       (COND ((AND FLG DEFNS)
				      /, |and|)
				     (DEFNS |and|))))
		 (COND (DEFNS |the| (PLURAL? DEFNS |definitions| |definition|)
			 |of|
			 (!LIST DEFNS)))
		 (COND ((OR FLG LEMMAS DEFNS)
			(PLURAL? NUMBER (? (|inform| |us|)
					   (|establish|)
					   (|can| |be| |used| |to|
						  (? (|prove|)
						     (|show|)
						     (|establish|))))
				 (? (|establishes|)
				    (|informs| |us|)
				    (|can| |be| |used| |to|
					   (? (|prove|)
					      (|show|)
					      (|establish|)))))
			|that|)
		       (T (? (|it| |is| |obvious| |that|)
			     (|obviously|)
			     (|clearly|))))
		 |the| |measure| (!PPR MEASURE NIL)
		 |decreases| |according| |to| |the| |well-founded| |relation|
		 (!PPR RELATION NIL)
		 |in|)))

(DEFUN !LIST (*LST*)
  (MAPRINEVAL *LST* *INDENT* *FILE* NIL NIL (PQUOTE /,)
	      (COND ((CDDR *LST*)
		     (PQUOTE (PROGN /, |and|)))
		    (T (PQUOTE |and|)))))

(DEFUN MAPRINEVAL (*LST* *INDENT* *FILE* *LEFT* *RIGHT* *SEPR* *FINALSEPR*)
  (AND *LEFT* (PRINEVAL1 *LEFT*))
  (COND ((PAIRP *LST*)
	 (COND ((CDR *LST*)
		(LOOP FOR TAIL ON *LST*
		      DO (PRINEVAL1 (CAR TAIL))
		      (COND ((NULL (CDR TAIL))
			     NIL)
			    ((NULL (CDDR TAIL))
			     (AND *FINALSEPR* (PRINEVAL1 *FINALSEPR*)))
			    (T (AND *FINALSEPR* (PRINEVAL1 *SEPR*))))))
	       (T (PRINEVAL1 (CAR *LST*))))))
  (AND *RIGHT* (PRINEVAL1 *RIGHT*)))

(DEFUN NOTICE-CLAUSE (CL COL BROTHER-NO)
  (CAR (SETQ CLAUSE-ALIST (CONS (LIST CL (OR COL 0)
				      BROTHER-NO)
				CLAUSE-ALIST))))

(DEFUN PEVAL (FORM)
  (COND ((ATOM FORM)
	 (COND ((SYMBOLP FORM)
		(COND ((OR (EQ FORM NIL)
			   (EQ FORM T))
		       FORM)
		      (T (PEVALV FORM))))
	       ((NUMBERP FORM) FORM)
	       (T
		(ERROR1 (PQUOTE (PROGN |Illegal| PEVAL |form|
				       /, (!PPR TERM NIL) /.))
			(BINDINGS (QUOTE TERM) FORM)
			(QUOTE HARD)))))
	((OR (EQ (CAR FORM) (QUOTE PQUOTE))
	     (EQ (CAR FORM) (QUOTE QUOTE)))
	 (CADR FORM))
	((MEMQ (CAR FORM) PRINEVAL-FNS)
	 (PEVAL-APPLY (CAR FORM)
		      (LOOP FOR X IN (CDR FORM) COLLECT (PEVAL X))))
	(T (ERROR1 (PQUOTE (PROGN |Illegal| PEVAL |form| /,
				  (!PPR TERM NIL) /.))
		   (BINDINGS (QUOTE TERM) FORM)
		   (QUOTE HARD)))))
(DEFUN PEVAL-APPLY (FN ARGS)
  (SELECTQ FN
    (AND (COND ((NULL ARGS) T)
	       ((MEMQ NIL ARGS) NIL)
	       (T (CAR (LAST ARGS)))))
    (OR (LOOP FOR X IN ARGS THEREIS X))
    (FN-SYMB (FN-SYMB (CAR ARGS)))
    (FFN-SYMB (FFN-SYMB (CAR ARGS)))
    (ARGN (ARGN (CAR ARGS) (CADR ARGS)))
    (FARGN (FARGN (CAR ARGS) (CADR ARGS)))
    (SARGS (SARGS (CAR ARGS)))
    (FARGS (FARGS (CAR ARGS)))
    (QUOTEP (QUOTEP (CAR ARGS)))
    (FQUOTEP (FQUOTEP (CAR ARGS)))
    (OTHERWISE (APPLY FN ARGS))))

(DEFUN PEVALV (X)
  (LET (TEMP)
    (COND ((SETQ TEMP (ASSQ X *ALIST*))
	   (CDR TEMP))
	  (T (ERROR1 (PQUOTE (PROGN (!PPR X NIL)
				    |is| |an| |unbound| |atom| |in|
				    PRINEVAL !))
		     (LIST (CONS (QUOTE X) X))
		     (QUOTE HARD))))))

(DEFUN PLURALP (X)
  (NOT (OR (EQUAL X 1)
	   (AND (PAIRP X)
		(ATOM (CDR X))))))

(DEFUN !PPR-LIST (*LST*)
  (MAPRINEVAL (LOOP FOR X IN *LST* COLLECT (LIST (QUOTE !PPR)
						 (KWOTE X)
						 NIL))
	      *INDENT* *FILE* NIL NIL (PQUOTE /,)
	      (COND ((CDDR *LST*)
		     (PQUOTE (PROGN /, |and|)))
		    (T (PQUOTE |and|)))))

(DEFUN !PPR (X PUNCT)
  (LET (NCHARS)
    (SETQ X (EXPAND-PPR-MACROS X))
    (SETQ NCHARS (FLATSIZE X))
    (COND ((> (+ 2 (MAX (IPOSITION *FILE* NIL NIL)
			*INDENT*)
		 NCHARS)
	      (LINEL *FILE*))
	   (COND ((AND (<= (+ *INDENT* NCHARS)
			   (LINEL *FILE*))
		       (< NCHARS 25))
		  (ITERPRI *FILE*)
		  (ISPACES *INDENT* *FILE*)
		  (IPRINC X *FILE*)
		  (AND PUNCT (PRINEVAL1 PUNCT)))
		 (T (PRINEVAL1 (PQUOTE (PROGN /: //)))
		    (PPRINDENT X (+ *INDENT* 6)
			       (COND (PUNCT (STRING-LENGTH PUNCT))
				     (T 0))
			       *FILE*)
		    (AND PUNCT (PRINEVAL1 PUNCT))
		    (ITERPRI *FILE*))))
	  (T (ISPACES (- *INDENT* (IPOSITION *FILE* NIL NIL))
		      *FILE*)
	     (OR (= (IPOSITION *FILE* NIL NIL)
		    *INDENT*)
		 (ISPACES 1 *FILE*))
	     (IPRINC X *FILE*)
	     (AND PUNCT (PRINEVAL1 PUNCT))))
    (OR PUNCT (SETQ LAST-PRINEVAL-CHAR (COND ((PAIRP X)
					      (QUOTE /)))
					     (T (QUOTE X)))))
    NIL))

(DEFUN PRIN5* (X)
  (LET (SPACES (*NOPOINT T))
    (SETQ SPACES (COND ((= 0 (IPOSITION *FILE* NIL NIL))
			0)
		       ((EQ LAST-PRINEVAL-CHAR (QUOTE /.))
			2)
		       ((EQ LAST-PRINEVAL-CHAR (QUOTE /:))
			2)
		       (T 1)))
    (COND ((MEMQ X (QUOTE (// /# /. ! ? /, /:)))
	   (COND ((EQ X (QUOTE //))
		  (ITERPRI *FILE*))
		 ((EQ X (QUOTE /#))
		  (ISPACES (- *INDENT* (IPOSITION *FILE* NIL NIL))
			   *FILE*)
		  (ISPACES (- PARAGRAPH-INDENT 2)
			   *FILE*)
		  (SETQ LAST-PRINEVAL-CHAR (QUOTE /.)))
		 ((OR (EQ X (QUOTE /,))
		      (EQ X (QUOTE /:)))
		  (COND ((AND (NOT (MEMQ LAST-PRINEVAL-CHAR (QUOTE (/. /, /:))))
			      (NOT (= 0 (IPOSITION *FILE* NIL NIL))))
			 (ISPACES
			   (- *INDENT* (IPOSITION *FILE* NIL NIL)) *FILE*)
			 (IPRINC X *FILE*)
			 (SETQ LAST-PRINEVAL-CHAR X))))
		 ((OR (EQ X (QUOTE /.))
		      (EQ X (QUOTE !))
		      (EQ X (QUOTE ?)))
		  (ISPACES (- *INDENT* (IPOSITION *FILE* NIL NIL)) *FILE*)
		  (IPRINC X *FILE*)
		  (SETQ LAST-PRINEVAL-CHAR (QUOTE /.)))
		 (T (ERROR1 (PQUOTE (PROGN |The| |code| |for| PRIN5* |is|
					   |inconsistent| /: |the| MEMQ |says|
					   |one| |thing|
					   |and| |the| COND |says| |another|
					   /.))
			    (BINDINGS)
			    (QUOTE HARD)))))
	  ((EQ X NIL) NIL)
	  (T
	   (ISPACES (- *INDENT* (IPOSITION *FILE* NIL NIL)) *FILE*)
	   (COND ((> (+ (IPOSITION *FILE* NIL NIL) SPACES (STRING-LENGTH X) 1)
		     (LINEL *FILE*))
		  (ITERPRI *FILE*)
		  (ISPACES *INDENT* *FILE*))
		 (T (ISPACES SPACES *FILE*)))
	   (COND ((NUMBERP X)(IPRINC X *FILE*))
		 (T (COND ((EQ LAST-PRINEVAL-CHAR (QUOTE /.))
			   (IPRINC (ASCII (CHAR-UPCASE (OUR-GETCHARN X 1))) *FILE*)
			   (LOOP FOR I FROM 2 TO (STRING-LENGTH X)
				 DO (IPRINC (OUR-GETCHAR X I) *FILE*)))
			  (T (IPRINC X *FILE*)))))
	   (SETQ LAST-PRINEVAL-CHAR NIL)))
    NIL))

(DEFUN PRINEVAL (FORM *ALIST* *INDENT* *FILE*)
  (PRINEVAL1 FORM))

(DEFUN PRINEVAL1 (*FORM*)
  (COND ((ATOM *FORM*)
	 (PRIN5* (COND ((FIXP *FORM*)
			(SPELL-NUMBER *FORM*))
		       (T *FORM*))))
	(T (SELECTQ (CAR *FORM*)
	     (@ (PRINEVAL1 (PEVAL (CADR *FORM*))))
	     (? (LOOP FOR *FORM*
		      IN (NTH (1+ (RANDOM-NUMBER (LENGTH (CDR *FORM*))))
			      *FORM*)
		      DO (PRINEVAL1 *FORM*)))
	     (COND (LOOP FOR *FORM* IN (CDR *FORM*)
			 THEREIS
			 (COND ((PEVAL (CAR *FORM*))
				(LOOP FOR *FORM* IN (CDR *FORM*)
				      DO (PRINEVAL1 *FORM*))
				T))))
	     (PLURAL? (COND ((PLURALP (PEVAL (CADR *FORM*)))
			     (PRINEVAL1 (CADDR *FORM*)))
			    (T (PRINEVAL1 (CADDDR *FORM*)))))
	     (PROGN (LOOP FOR *FORM* IN (CDR *FORM*)
			  DO (PRINEVAL1 *FORM*)))
	     (OTHERWISE (PEVAL *FORM*))))))

(DEFUN PRINT-DEFN-MSG (NAME ARGS)
  (PROG (TEMPS MEASURE RELATION LEMMAS FLG CONCL TIME N DEFNS)
	(SETQ LAST-PRIN5-WORD (QUOTE /.))
	(SETQ TIME (TIME-IN-60THS))
	(COND (IN-BOOT-STRAP-FLG
	       (SETQ IOTHMTIME (TIME-DIFFERENCE (TIME-IN-60THS)
						TIME))
	       (RETURN NIL)))
	(SETQ TEMPS (GET1 NAME (QUOTE JUSTIFICATIONS)))
	(COND
	  ((NOT (TOTAL-FUNCTIONP NAME))
	   (ERROR1 (PQUOTE (PROGN |The| |admissibility| |of| (!PPR NAME NIL)
				  |has| |not| |been| |established| /. |We|
				  |will| |assume| |that| |there| |exists| |a|
				  |function| |satisfying| |this|
				  |definition| /. |An| |induction|
				  |principle| |for| |this| |function| |has|
				  |also| |been| |assumed| /, |corresponding|
				  |to| |the| |obvious| |subgoal| |induction|
				  |for| |the| |function| /. |These|
				  |assumptions| |may| |render| |the| |theory|
				  |inconsistent| /. // //))
		   (BINDINGS (QUOTE NAME)
			     NAME)
		   (QUOTE WARNING)))
	  (T
	   (SETQ N (1- (LENGTH TEMPS)))
	   (PRINEVAL (PQUOTE (PROGN /#))
		     (BINDINGS)
		     0 PROVE-FILE)
	   (LOOP FOR TEMP IN TEMPS AS I FROM 1
		 DO
		 (SETQ MEASURE (ACCESS JUSTIFICATION MEASURE-TERM TEMP))
		 (SETQ RELATION (ACCESS JUSTIFICATION RELATION TEMP))
		 (SETQ FLG NIL)
		 (SETQ LEMMAS NIL)
		 (SETQ DEFNS NIL)
		 (LOOP FOR X IN (ACCESS JUSTIFICATION LEMMAS TEMP)
		       DO (COND ((EQ X (QUOTE ZERO))
				 (SETQ FLG T))
				((GET1 X (QUOTE TYPE-PRESCRIPTION-LST))
				 (SETQ DEFNS (CONS X DEFNS)))
				(T (SETQ LEMMAS (CONS X LEMMAS)))))
		 (PRINEVAL
		   (PQUOTE (PROGN (COND (FINALLY? (COND ((EQUAL N 2)
							 |In| |addition|)
							(T |Finally|)) /,))
				  (@ JUSTIFICATION-SENTENCE)
				  |each| |recursive| |call| /.
				  (COND ((EQUAL I 1)
					 |Hence| /, (!PPR NAME NIL)
					 |is| |accepted| |under| |the|
					 (? (|principle| |of| |definition|)
					    (|definitional| |principle|))
					 /.
					 (COND ((EQUAL N 1)
						|the| |definition| |of|
						(!PPR NAME NIL)
						|can| |be| |justified|
						|in| |another|
						|way| /.)
					       (OTHERS
						|there| |are| (@ N)
						|other|
						(? (|explanations| |of|)
						   (|measures|
						     |and| |well-founded|
						     |functions|
						     |explaining|))
						|the| |recursion|
						|above| /.))))))
		   (BINDINGS (QUOTE N)
			     N
			     (QUOTE NAME)
			     NAME
			     (QUOTE I)
			     I
			     (QUOTE JUSTIFICATION-SENTENCE)
			     (JUSTIFICATION-SENTENCE)
			     (QUOTE RELATION)
			     RELATION
			     (QUOTE MEASURE)
			     MEASURE
			     (QUOTE DEFNS)
			     DEFNS
			     (QUOTE LEMMAS)
			     LEMMAS
			     (QUOTE FLG)
			     FLG
			     (QUOTE NUMBER)
			     (LENGTH (ACCESS JUSTIFICATION LEMMAS TEMP))
			     (QUOTE FINALLY?)
			     (AND (NOT (EQUAL I 1))
				  (NOT (EQUAL N 1))
				  (EQUAL I (ADD1 N)))
			     (QUOTE OTHERS)
			     (GREATERP N 1))
		   0 PROVE-FILE))))
	(COND ((NOT (= TYPE-SET-UNKNOWN (CAR (TYPE-PRESCRIPTION NAME))))
	       (SETQ TEMP-TEMP
		     (CONS (DUMB-CONVERT-TYPE-SET-TO-TYPE-RESTRICTION-TERM
			     (CAR (TYPE-PRESCRIPTION NAME))
			     (CONS NAME ARGS))
			   (LOOP FOR FLG IN (CDR (TYPE-PRESCRIPTION NAME))
				 AS I FROM 0 WHEN FLG
				 COLLECT (LIST (QUOTE EQUAL)
					       (CONS NAME ARGS)
					       (NTH I ARGS)))))
	       (SETQ CONCL (COND ((NULL (CDR TEMP-TEMP))
				  (CAR TEMP-TEMP))
				 (T (CONS (QUOTE OR)
					  TEMP-TEMP))))
	       (PRINEVAL (PQUOTE (PROGN (? (|Note| |that|)
					   (|Observe| |that|)
					   (|From| |the| |definition| |we|
						   |can| |conclude| |that|))
					(!PPR CONCL NIL)
					|is| |a| |theorem| /.))
			 (BINDINGS (QUOTE CONCL)
				   CONCL)
			 0 PROVE-FILE)))
	(SETQ IOTHMTIME (TIME-DIFFERENCE (TIME-IN-60THS)
					 TIME))
	(RETURN NIL)))

(DEFUN TH-IFY (N)
  (SELECTQ N
    (1 (QUOTE |first|))
    (2 (QUOTE |second|))
    (3 (QUOTE |third|))
    (4 (QUOTE |fourth|))
    (5 (QUOTE |fifth|))
    (6 (QUOTE |sixth|))
    (7 (QUOTE |seventh|))
    (8 (QUOTE |eighth|))
    (9 (QUOTE |ninth|))
    (10 (QUOTE |tenth|))
    (11 (QUOTE |11th|))
    (12 (QUOTE |12th|))
    (13 (QUOTE |13th|))
    (OTHERWISE
     (COND ((FIXP N)
	    (PACK (NCONC (EXPLODE-NUMBER N)
			 (SELECTQ (REMAINDER N 10)
			   (1 (QUOTE |st|))
			   (2 (QUOTE |nd|))
			   (3 (QUOTE |rd|))
			   (OTHERWISE
			    (QUOTE |th|))))))
	   (T N)))))

(DEFUN UN-NOTICE-CLAUSE (CL)
  (SETQ TEMP-TEMP (ASSQ CL CLAUSE-ALIST))
  (COND ((NULL TEMP-TEMP)
	 (ERROR1 (PQUOTE (PROGN UN-NOTICE-CLAUSE |was| |called|
				|on| |a| |clause|
				|not| |in| CLAUSE-ALIST !))
		 NIL
		 (QUOTE HARD))))
  (SETQ CLAUSE-ALIST (DELQ TEMP-TEMP CLAUSE-ALIST))
  TEMP-TEMP)